Nuprl Lemma : ocgrp_inverse
13,42
postcript
pdf
g
:OGrp,
x
:|
g
|. (
x
* (~(
x
))) = e
|
g
| & ((~(
x
)) *
x
) = e
|
g
|
latex
Up
groups
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Inverse(
T
;
op
;
id
;
inv
)
Lemmas
ocgrp
wf
,
ocgrp
properties
origin
g:OGrp, x:|g|. (x * (~(x))) = e 
|g| & ((~(x)) * x) = e |g| g:OGrp, x:|g|. (x * (~(x))) = e |g| & ((~(x)) * x) = e |g| Tx:A. B(x)